Nuprl Lemma : es-prior-interface-causl
11,40
postcript
pdf
es
:ES,
X
:AbsInterface(Top),
e
:E. (
(
e
prior(
X
)))
(prior(
X
)(
e
) <
e
)
latex
Definitions
(
e
<
e'
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
s
=
t
,
(
e
<loc
e'
)
,
prior(
X
)
,
X
(
e
)
,
e
X
,
b
,
x
:
A
B
(
x
)
,
P
Q
,
E
,
x
:
A
.
B
(
x
)
,
Top
,
AbsInterface(
A
)
,
ES
Lemmas
es-prior-interface-locl
,
event
system
wf
,
top
wf
,
es-interface
wf
,
es-E
wf
,
es-causl
wf
,
assert
wf
origin
es:ES, X:AbsInterface(Top), e:E. (
(e 
prior(X))) 
(prior(X)(e) < e) es:ES, X:AbsInterface(Top), e:E. ((e prior(X))) (prior(X)(e) < e) 
B(x) Xb
B(x) Qx:A. B(x)